LTL: G(((!g_0 & !g_1 & (!g_2 | !g_3)) | (!g_2 & !g_3 & (!g_0 | !g_1))) & (r_0 -> Fg_0) & (r_1 -> Fg_1) & (r_2 -> Fg_2) & (r_3 -> Fg_3))
Input APs: [r_0, r_1, r_2, r_3]
Illegal letters: 176 out of the 256 letters (68.75%) are illegal.
¬LTL: !G(((!g_0 & !g_1 & (!g_2 | !g_3)) | (!g_2 & !g_3 & (!g_0 | !g_1))) & (r_0 -> Fg_0) & (r_1 -> Fg_1) & (r_2 -> Fg_2) & (r_3 -> Fg_3))
NonDet Buchi of negated LTL:
Universal CoBuchi of LTL:
Expanded K-CoBuchi for K=0:
kUCB complement:
The empty word is accepted.
Closing table ...
Hypothesis table:
Table:
0: 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
Number of states: 2
Hypothesis is NOT realisable.
Strategy:
Moore machine:
No counterexample found. For this K, the formula is not realisable.
Timers for K = 0:
We have a proof of unrealisability for K = 0
However this is not a proof for the general formula. We need to increment K.
Counterexample: cycle{!g_0 & !g_1 & g_2 & g_3 & !r_0 & !r_1 & r_2 & r_3}
Expanded K-CoBuchi for K=1:
kUCB complement:
The empty word is accepted.
Closing table ...
Hypothesis table:
Table:
0: 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
Number of states: 2
Hypothesis is realisable.
Strategy:
Mealy machine 1:
Original (symbolic) counterexample: cycle{!g_0 & !g_1 & !g_2 & r_0}
Counterexample: cycle{!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1
2: 1 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Number of states: 3
Hypothesis is realisable.
Strategy:
Mealy machine 2:
Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & r_1; cycle{g_0 & !g_1 & !g_2 & !g_3 & !r_1 & !r_2}
Counterexample: !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1
2: 1 0 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1
4: 1 1 0
2: 1 0 1
3: 1 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Number of states: 5
Hypothesis is realisable.
Strategy:
Mealy machine 4:
Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_2 & !r_3}
Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1
4: 1 1 0 0
2: 1 0 1 0
3: 1 0 0 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
3: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1
4: 1 1 0 0
2: 1 0 1 0
3: 1 0 0 1
5: 1 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
3: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Number of states: 6
Hypothesis is NOT realisable.
Strategy:
Moore machine:
No counterexample found. For this K, the formula is not realisable.
Timers for K = 1:
We have a proof of unrealisability for K = 1
However this is not a proof for the general formula. We need to increment K.
Counterexample: cycle{!g_0 & !g_1 & g_2 & g_3 & !r_0 & r_1 & r_2 & r_3}
Expanded K-CoBuchi for K=2:
kUCB complement:
The empty word is accepted.
Closing table ...
Hypothesis table:
Table:
0: 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
Number of states: 2
Hypothesis is realisable.
Strategy:
Mealy machine 1:
Original (symbolic) counterexample: cycle{!g_0 & !g_1 & !g_2 & r_0}
Counterexample: cycle{!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1
2: 1 0 1
3: 1 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Number of states: 4
Hypothesis is realisable.
Strategy:
Mealy machine 3:
Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & r_1; cycle{g_0 & !g_1 & !g_2 & !g_3 & !r_1 & !r_2}
Counterexample: !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1
2: 1 0 1 1 1
3: 1 0 0 1 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1
5: 1 1 1 0 1
9: 1 1 1 0 0
8: 1 1 0 0 0
2: 1 0 1 1 1
4: 1 0 1 0 1
10: 1 0 1 0 0
3: 1 0 0 1 1
6: 1 0 0 0 1
7: 1 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Number of states: 11
Hypothesis is realisable.
Strategy:
Mealy machine 10:
Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_2 & !r_3}
Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1
9: 1 1 1 0 0 0 0
8: 1 1 0 0 0 0 0
2: 1 0 1 1 1 0 1
4: 1 0 1 0 1 1 1
10: 1 0 1 0 0 0 0
3: 1 0 0 1 1 0 0
6: 1 0 0 0 1 0 0
7: 1 0 0 0 0 1 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1
9: 1 1 1 0 0 0 0
8: 1 1 0 0 0 0 0
2: 1 0 1 1 1 0 1
4: 1 0 1 0 1 1 1
11: 1 0 1 0 1 0 1
10: 1 0 1 0 0 0 0
3: 1 0 0 1 1 0 0
6: 1 0 0 0 1 0 0
7: 1 0 0 0 0 1 1
12: 1 0 0 0 0 0 1
13: 1 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Number of states: 14
Hypothesis is realisable.
Strategy:
Mealy machine 12:
Original (symbolic) counterexample: cycle{g_0 & !g_1 & !g_2 & !g_3 & r_2; !g_0 & g_1 & !g_2 & !g_3 & !r_2 & r_3}
Counterexample: cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3; !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3}
Shortest finite counterexample: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1
9: 1 1 1 0 0 0 0 0 0
8: 1 1 0 0 0 0 0 0 0
2: 1 0 1 1 1 0 1 1 1
4: 1 0 1 0 1 1 1 1 1
11: 1 0 1 0 1 0 1 1 1
10: 1 0 1 0 0 0 0 0 0
3: 1 0 0 1 1 0 0 0 1
6: 1 0 0 0 1 0 0 0 1
7: 1 0 0 0 0 1 1 1 0
12: 1 0 0 0 0 0 1 1 0
13: 1 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1
9: 1 1 1 0 0 0 0 0 0
8: 1 1 0 0 0 0 0 0 0
2: 1 0 1 1 1 0 1 1 1
4: 1 0 1 0 1 1 1 1 1
11: 1 0 1 0 1 0 1 1 1
14: 1 0 1 0 1 0 1 0 1
10: 1 0 1 0 0 0 0 0 0
3: 1 0 0 1 1 0 0 0 1
6: 1 0 0 0 1 0 0 0 1
7: 1 0 0 0 0 1 1 1 0
12: 1 0 0 0 0 0 1 1 0
15: 1 0 0 0 0 0 1 0 0
13: 1 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
Number of states: 16
Hypothesis is NOT realisable.
Strategy:
Moore machine:
Counterexample: !g_0 & !g_1 & g_2 & !g_3 & !r_0 & r_1 & r_2 & r_3; !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3; !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3}
Shortest finite counterexample: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & r_1 & r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1
9: 1 1 1 0 0 0 0 0 0 0 1
8: 1 1 0 0 0 0 0 0 0 0 1
2: 1 0 1 1 1 0 1 1 1 0 1
4: 1 0 1 0 1 1 1 1 1 1 1
11: 1 0 1 0 1 0 1 1 1 0 1
14: 1 0 1 0 1 0 1 0 1 0 1
10: 1 0 1 0 0 0 0 0 0 0 1
3: 1 0 0 1 1 0 0 0 1 0 0
6: 1 0 0 0 1 0 0 0 1 0 0
7: 1 0 0 0 0 1 1 1 0 1 0
12: 1 0 0 0 0 0 1 1 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0
13: 1 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1
9: 1 1 1 0 0 0 0 0 0 0 1
8: 1 1 0 0 0 0 0 0 0 0 1
2: 1 0 1 1 1 0 1 1 1 0 1
4: 1 0 1 0 1 1 1 1 1 1 1
11: 1 0 1 0 1 0 1 1 1 0 1
16: 1 0 1 0 1 0 1 0 1 1 1
14: 1 0 1 0 1 0 1 0 1 0 1
10: 1 0 1 0 0 0 0 0 0 0 1
3: 1 0 0 1 1 0 0 0 1 0 0
6: 1 0 0 0 1 0 0 0 1 0 0
7: 1 0 0 0 0 1 1 1 0 1 0
12: 1 0 0 0 0 0 1 1 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0
15: 1 0 0 0 0 0 1 0 0 0 0
13: 1 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
Number of states: 18
Hypothesis is NOT realisable.
Strategy:
Moore machine:
Counterexample: g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & !r_3; !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3; !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3}
Shortest finite counterexample: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1 0 1
9: 1 1 1 0 0 0 0 0 0 0 1 0 0
8: 1 1 0 0 0 0 0 0 0 0 1 0 0
2: 1 0 1 1 1 0 1 1 1 0 1 0 1
4: 1 0 1 0 1 1 1 1 1 1 1 1 1
11: 1 0 1 0 1 0 1 1 1 0 1 0 1
16: 1 0 1 0 1 0 1 0 1 1 1 0 1
14: 1 0 1 0 1 0 1 0 1 0 1 1 1
10: 1 0 1 0 0 0 0 0 0 0 1 0 0
3: 1 0 0 1 1 0 0 0 1 0 0 0 0
6: 1 0 0 0 1 0 0 0 1 0 0 0 0
7: 1 0 0 0 0 1 1 1 0 1 0 1 0
12: 1 0 0 0 0 0 1 1 0 0 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0 1 0
13: 1 0 0 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1 0 1
9: 1 1 1 0 0 0 0 0 0 0 1 0 0
8: 1 1 0 0 0 0 0 0 0 0 1 0 0
2: 1 0 1 1 1 0 1 1 1 0 1 0 1
4: 1 0 1 0 1 1 1 1 1 1 1 1 1
11: 1 0 1 0 1 0 1 1 1 0 1 0 1
16: 1 0 1 0 1 0 1 0 1 1 1 0 1
14: 1 0 1 0 1 0 1 0 1 0 1 1 1
18: 1 0 1 0 1 0 1 0 1 0 1 0 1
10: 1 0 1 0 0 0 0 0 0 0 1 0 0
3: 1 0 0 1 1 0 0 0 1 0 0 0 0
6: 1 0 0 0 1 0 0 0 1 0 0 0 0
7: 1 0 0 0 0 1 1 1 0 1 0 1 0
12: 1 0 0 0 0 0 1 1 0 0 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0 1 0
19: 1 0 0 0 0 0 1 0 0 0 0 0 0
20: 1 0 0 0 0 0 0 0 0 0 0 0 1
13: 1 0 0 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Number of states: 21
Hypothesis is NOT realisable.
Strategy:
Moore machine:
Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3; !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1
9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0
8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0
2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1
4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1
11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1
16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1
14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1
18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0
3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0
6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0
7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0
12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0
19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0
20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1
13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1
9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0
8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0
2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1
4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1
11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1
16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1
14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1
21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1
22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1
18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0
10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0
3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0
6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0
7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0
12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0
19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0
20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1
13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Number of states: 24
Hypothesis is NOT realisable.
Strategy:
Moore machine:
Counterexample: !g_0 & !g_1 & g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3; !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3}
Shortest finite counterexample: [!g_0 & !g_1 & g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 1 1
9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 1 0
8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0
2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 1 1
4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 0 1
11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 1
16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1
14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 0 1
21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1
22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1
18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 0 0
10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 1 0
3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1
6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1
7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0
12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0
19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0
20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0
13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
16: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 1 1
9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 1 0
8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0
2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 1 1
4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 0 1
11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 1
16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1
14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 0 1
21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1
22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1
24: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1
18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 0 0
10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 1 0
25: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0
3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1
6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1
7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0
12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0
19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0
20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0
13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
16: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
Number of states: 26
Hypothesis is NOT realisable.
Strategy:
Moore machine:
Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3; !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3; g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3; !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 1 1 0 1 1
9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 1
8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 1
2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 1 1 1 1 1
4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 0 1 0 0 1
11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 1 0 0 1
16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 0 1
14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 0 1 1 0 1
21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 0 1
22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 0 1
24: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 1
18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 0 1
23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 0 1
10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 1 0 0 0 1
25: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1
3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1 0 1 0
6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0
7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0 0 0 0
12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0
19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0
20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 1 0 0
13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
16: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
17: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
19: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 1 1 0 1 1
9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 1
8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 1
2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 1 1 1 1 1
4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 0 1 0 0 1
11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 1 0 0 1
16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 0 1
14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 0 1 1 0 1
21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 0 1
22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 0 1
24: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 1
18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 0 1
26: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 0 1
23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 0 1
10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 1 0 0 0 1
25: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1
3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1 0 1 0
27: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 0 1 0
6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0
7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0 0 0 0
12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0
17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0 0 0 0
15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0
19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0
20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 1 0 0
28: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0
13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
26: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & !r_3]
27: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
28: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
16: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
17: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
18: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
19: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
Number of states: 29
Hypothesis is NOT realisable.
Strategy:
Moore machine:
No counterexample found. For this K, the formula is not realisable.
Timers for K = 2:
We have a proof of unrealisability for K = 2
However this is not a proof for the general formula. We need to increment K.
Counterexample: cycle{!g_0 & !g_1 & g_2 & g_3 & r_0 & r_1 & r_2 & r_3}
Expanded K-CoBuchi for K=3:
kUCB complement:
The empty word is accepted.
Closing table ...
Hypothesis table:
Table:
0: 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
Number of states: 2
Hypothesis is realisable.
Strategy:
Mealy machine 1:
Original (symbolic) counterexample: cycle{!g_0 & !g_1 & !g_2 & r_0}
Counterexample: cycle{!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1
2: 1 0 1 1
4: 1 0 0 1
3: 1 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
Number of states: 5
Hypothesis is realisable.
Strategy:
Mealy machine 4:
Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & r_1; cycle{g_0 & !g_1 & !g_2 & !g_3 & !r_1 & !r_2}
Counterexample: !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1
2: 1 0 1 1 1 1 1
4: 1 0 0 1 1 1 1
3: 1 0 0 0 1 1 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1
6: 1 1 1 1 0 1 1
12: 1 1 1 1 0 0 1
15: 1 1 1 1 0 0 0
11: 1 1 0 0 0 0 0
2: 1 0 1 1 1 1 1
5: 1 0 1 1 0 1 1
13: 1 0 1 1 0 0 1
16: 1 0 1 1 0 0 0
4: 1 0 0 1 1 1 1
7: 1 0 0 1 0 1 1
10: 1 0 0 1 0 0 1
17: 1 0 0 1 0 0 0
3: 1 0 0 0 1 1 1
8: 1 0 0 0 0 1 1
14: 1 0 0 0 0 0 1
9: 1 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
Number of states: 18
Hypothesis is realisable.
Strategy:
Mealy machine 17:
Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_2 & !r_3}
Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1 1 1 1
6: 1 1 1 1 0 1 1 0 1 1
12: 1 1 1 1 0 0 1 0 0 1
15: 1 1 1 1 0 0 0 0 0 0
11: 1 1 0 0 0 0 0 0 0 1
2: 1 0 1 1 1 1 1 0 1 1
5: 1 0 1 1 0 1 1 1 1 1
13: 1 0 1 1 0 0 1 0 0 1
16: 1 0 1 1 0 0 0 0 0 0
4: 1 0 0 1 1 1 1 0 0 1
7: 1 0 0 1 0 1 1 0 0 1
10: 1 0 0 1 0 0 1 1 1 1
17: 1 0 0 1 0 0 0 0 0 0
3: 1 0 0 0 1 1 1 0 0 1
8: 1 0 0 0 0 1 1 0 0 0
14: 1 0 0 0 0 0 1 0 0 0
9: 1 0 0 0 0 0 0 1 1 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
8: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Closing table ...
Hypothesis table:
Table:
0: 1 1 1 1 1 1 1 1 1 1
6: 1 1 1 1 0 1 1 0 1 1
12: 1 1 1 1 0 0 1 0 0 1
15: 1 1 1 1 0 0 0 0 0 0
11: 1 1 0 0 0 0 0 0 0 1
23: 1 1 0 0 0 0 0 0 0 0
2: 1 0 1 1 1 1 1 0 1 1
5: 1 0 1 1 0 1 1 1 1 1
18: 1 0 1 1 0 1 1 0 1 1
13: 1 0 1 1 0 0 1 0 0 1
16: 1 0 1 1 0 0 0 0 0 0
4: 1 0 0 1 1 1 1 0 0 1
7: 1 0 0 1 0 1 1 0 0 1
10: 1 0 0 1 0 0 1 1 1 1
20: 1 0 0 1 0 0 1 0 1 1
24: 1 0 0 1 0 0 1 0 0 1
17: 1 0 0 1 0 0 0 0 0 0
3: 1 0 0 0 1 1 1 0 0 1
19: 1 0 0 0 1 1 1 0 0 0
8: 1 0 0 0 0 1 1 0 0 0
14: 1 0 0 0 0 0 1 0 0 0
9: 1 0 0 0 0 0 0 1 1 1
22: 1 0 0 0 0 0 0 0 1 1
25: 1 0 0 0 0 0 0 0 0 1
21: 1 0 0 0 0 0 0 0 0 0
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
21: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
8: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
Number of states: 26
Hypothesis is realisable.
Strategy:
Mealy machine 25:
Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3; !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3; g_0 & !g_1 & !g_2 & !g_3 & !r_2 & r_3; !g_0 & g_1 & !g_2 & !g_3 & !r_2 & r_3}
Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3; !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3; g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3; !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3}
Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3]
Adding all suffixes of the counterexample to S.
Table after accounting for counterexample:
Table:
0: 1 1 1 1 1 1 1 1 1 1 1 1 1
6: 1 1 1 1 0 1 1 0 1 1 0 1 1
12: 1 1 1 1 0 0 1 0 0 1 0 0 1
15: 1 1 1 1 0 0 0 0 0 0 0 0 0
11: 1 1 0 0 0 0 0 0 0 1 0 0 1
23: 1 1 0 0 0 0 0 0 0 0 0 0 0
2: 1 0 1 1 1 1 1 0 1 1 1 1 1
5: 1 0 1 1 0 1 1 1 1 1 0 1 1
18: 1 0 1 1 0 1 1 0 1 1 0 1 1
13: 1 0 1 1 0 0 1 0 0 1 0 0 1
16: 1 0 1 1 0 0 0 0 0 0 0 0 0
4: 1 0 0 1 1 1 1 0 0 1 0 1 1
7: 1 0 0 1 0 1 1 0 0 1 0 1 1
10: 1 0 0 1 0 0 1 1 1 1 0 0 1
20: 1 0 0 1 0 0 1 0 1 1 0 0 1
24: 1 0 0 1 0 0 1 0 0 1 0 0 1
17: 1 0 0 1 0 0 0 0 0 0 0 0 0
3: 1 0 0 0 1 1 1 0 0 1 0 1 1
19: 1 0 0 0 1 1 1 0 0 0 0 0 1
8: 1 0 0 0 0 1 1 0 0 0 0 0 1
14: 1 0 0 0 0 0 1 0 0 0 0 0 1
9: 1 0 0 0 0 0 0 1 1 1 0 0 1
22: 1 0 0 0 0 0 0 0 1 1 0 0 0
25: 1 0 0 0 0 0 0 0 0 1 0 0 0
21: 1 0 0 0 0 0 0 0 0 0 0 0 1
1: 0
Prefixes:
0: []
1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
6: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
7: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
8: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
13: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
14: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
19: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
21: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
Suffixes:
0: []
1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
7: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
8: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
9: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3]
11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3]
12: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3]
Closing table ...